\requiere{f \textgreater max(fechas(SalidasDe(h,d)))}
\requiere{a \in habitaciones(h)}
\requiere{\neg checkinRegistrado(h, d, f, a)}
\requiere{\neg reservaConfirmada(h, d, f, a)}
\modifica{h}
\asegura{reservaConfirmada(h, d, f, a)}
\asegura{todoLoDemasNoCambia(h, pre(h), d, f, a)}
\asegura{(\forall r \selec reservas(pre(h))documento(r)==d \wedge fechaDesde(r)==f \wedge tipo(r)==tipo(a) \wedge confirmada(r)==False)(\exists! r_2 \selec reservas(h))documento(r)==documento(r_2) \wedge fechaDesde(r)==fechaDesde(r_2) \wedge fechaHasta(r)==fechaHasta(r_2) \wedge tipo(r)==tipo(r_2) \wedge confirmada(r_2)==True}
\asegura{(\forall r \selec reservas(pre(h)), /neg(documento(r)==d \wedge fechaDesde(r)==f \wedge tipo(r)==tipo(a) \wedge confirmada(r)==False)(\exists res \selec reservas(h))res==r}
\asegura{|reservas(pre(h))|==|reservas(h)|}
\aux{reservaConfirmada}{h : Hotel, d : DNI, f: Fecha, a : Habitacion}{\bool}{\\ 
(\exists r \selec reservas(h))
(documento(r) == d 
\wedge fechaDesde(r) == f 
\wedge tipo(r) == tipo(a) 
\wedge confirmada(r))}

\aux{todoLoDemasNoCambia}{h, preh: Hotel, d: DNI, f: Fecha, a: Habitacion}{\bool}{\\
nombre(h) == nombre(preh) \wedge cadena(h) == cadena(preh) \wedge habitaciones(h) == habitaciones(preh) \\
\wedge mismosHuespedes(h, preh, d) \wedge mismosCheckins(h, preh, d, f, a) \wedge preciosAccesorio(h)==preciosAccesorio(preh) \wedge TarifaHabitacionXDia(h)==TarifaHabitacionXDia(preh)}

\aux{mismosHuespedes}{h, preh: Hotel, d: DNI}{\bool}{\\ \IfThenElse{pertenece(d, huespedes(preh))\\}
{mismos(huespedes(h), huespedes(preh)) \\}
{mismos(huespedes(h), huespedes(preh) ++ [d])}}

\aux{mismosCheckins}{h, preh: Hotel, d: DNI, f: Fecha, a: Habitacion}{\bool}{\\ 
mismos(ingresos(h), ingresos(preh) ++ [((d, f), a)])}

\aux{fechas}{s:[CheckOut]}{[Fecha]}{[fechaCheckOut(x) | x \selec s]}

\aux{max}{xs:[Fecha]}{Fecha}{[x | x \selec xs, (\forall y \selec xs, x \neq y) x \textgreater y]}
